Nuprl Lemma : es_val_wf
0,22
postcript
pdf
es
:ES. es_val(
es
)
e
:E
kindcase(kind(
e
);
a
.es-V(
es
)(loc(
e
),
a
);
l
,
t
.es-M(
es
)(
l
,
t
) )
latex
Definitions
t
T
,
es_info(
es
)
,
es_val(
es
)
,
es-M(
es
)
,
loc(
e
)
,
es-V(
es
)
,
kind(
e
)
,
E
,
x
:
A
B
(
x
)
,
ES
,
x
:
A
B
(
x
)
,
Type
,
f
(
a
)
,
kindcase(
k
;
a
.
f
(
a
);
l
,
t
.
g
(
l
;
t
) )
,
x
:
A
.
B
(
x
)
Lemmas
event
system
wf
origin
es:ES. es_val(es) 
e:E
kindcase(kind(e); a.es-V(es)(loc(e),a); l,t.es-M(es)(l,t) ) es:ES. es_val(es) e:Ekindcase(kind(e); a.es-V(es)(loc(e),a); l,t.es-M(es)(l,t) ) T
B(x)B(x)x:A. B(x)